Diese Audiobeitrag wird von der Universität Erlangen Nürnberg präsentiert.

Erstmal noch zwei organisatorische Dinge.

Zum einen ist am Dienstag Feiertag.

Das heißt, der Übungsbetriebe findet nicht statt.

Aber am Montag und Donnerstag sind natürlich trotzdem Übungen.

Das heißt, ich würde Sie bitten, wenn Sie eine Dienstagsübung besuchen,

sich stattdessen in eine montags- oder donnerstagsgruppe zu setzen. am montag

wird sich es anbieten in eine der drei übungen zu gehen die nicht im blauen

hochhaus stattfinden weil das die vollste ist. aber das wird sich selber

irgendwie regeln müssen also wir können schlecht einen doodle einrichten wer

wohin gehen möchte. also bitte einfach selbstständig in eine

andere übungsgruppe gehen oder sich anderweitig informieren was stattgefunden

hat und was geübt wurde. und zweitens die meisten werden sie jetzt schon bemerkt

haben ich habe auch eine nachricht auf studon hinterlegt dass sich in der ersten

version des zweiten übungsplatz ein fehler eingeschlichen hatte der ist aber

schon am montag nachmittag korrigiert worden

also wer die das übungsblatt schon am wochenende runtergeladen hat sollte sich

noch die aktuelle version holen bevor er es bearbeitet sonst wird es eventuell

nicht funktionieren. okay dann können wir da weitermachen wo

wir letztes mal aufgehört haben und zwar haben wir im endeffekt ja jetzt schon

gelernt wie man mit einem thermoersetzungssystem umgeht wenn man

wissen will ob das terminiert und ob es konfluente ist. also terminierung da

braucht man ein bisschen diese kreativität mit dem polynomial finden und

konfluenz haben wir jetzt gelernt dass man die kritischen paare finden muss und

alle diese kritischen paare zusammenführen muss. allerdings haben wir

uns noch nicht beschäftigt warum das jetzt funktioniert. also wir haben die

beweise von diesen beiden wichtigen setzen noch aufgeschoben und das ist was wir

heute machen wollen. also zunächst hatten wir dieses critical

pair lemma beziehungsweise ist eigentlich das zweite aber das ist das was man

einfacher und schneller beweisen kann. und zwar schreibe ich es noch mal an. also das

critical pair lemma hat einfach ausgesagt dass diese lokale konfluenz

also was wir als wcr und weekly church rossa abgekürzt haben nichts anderes

bedeutet als alle kritischen paare und wir haben gesehen dass sie dass es

endlich viele geben muss wenn wir bestimmte endlichkeitsbedingungen auf

unser thermersetzungssystem verlangen dass alle kritischen paare zusammenführbar

sind. also dann wollen wir das mal beweisen und eine richtung von dem beweis

ist wie so oft auch wieder trivial. also das ist natürlich diese richtung hier

also wenn ich schon lokal konfluent bin dann sind natürlich meine kritischen

paare wieder nur eine instanz dieses ganzen. das heißt diese richtung hier ist

klar und wir müssen uns wieder nur mit der anderen richtung beschäftigen. also

dass das auch schon schon genügt. und dafür führen wir jetzt erstmal noch ein

bisschen notation ein für kontexte.

ich glaube der da drüben benutzt das mikrofon für zweisäle deswegen ist es

hier so leise. also notation wir sagen ein kontext ist gewissermaßen kleiner

als ein anderer kontext. genau dann wenn das der fall ist dass c entsteht

indem man in d irgendeinen anderen kontext einsetzt. also bildlich gesprochen

also ich habe hier irgendwie einen kontext d. ist auch so ein thermenbaum im

endeffekt. also kontexte sind ja auch baumförmig aufgebaut über diese

grammatik die ähnlich aussieht wie die von unserem thermen bis auf dieses loch.

und in dieses loch setze ich jetzt hier sagen wir hier ist das loch da setze ich